This disclosure is generally directed to the area of verification for integrated circuit (IC) designs. In particular, the disclosure is related to an improved approach for implementing equivalence checking functionality in electronic design automation (EDA) verification tools.
Today, ICs typically contain large numbers of circuit elements. Computer-aided design (CAD) and computer-aided engineering (CAE) tools are essential in assisting circuit designers to produce these complicated ICs. Circuit designs are typically represented in a user-specified hardware description language (HDL), which demonstrate the behavioral properties of the circuit.
Designers commonly utilize CAE software, or synthesis, to translate the behavioral representation, for example, a Register-Transfer-Level (RTL) description, into a implementation representation, for example, a gate-level representation. The synthesizer makes choices on the implementation architecture based on parameters such as timing, footprint, and power consumption. The result of the synthesis process, the gate-level representation, is referred to as the revised circuit, while the behavioral properties of the circuit, the RTL representation, is referred to as the golden circuit.
With increasing design complexity, formal verification (and particularly equivalence checking) becomes integral in the design process to ensure that the revised circuit is equivalent to the original specification, or golden circuit. In the verification of digital circuits, signals in the circuits are “compared” in some manner in order to draw a conclusion on the “correctness” of one or more properties of the circuits. For example, to determine if two circuits with identical state encoding will behave identically under some excitations, one can simply compare the simulated values of the corresponding state-points in the two circuits when the circuits are subjected to the same excitations.
In addition, one can show that the two circuits will behave identically under all possible excitations with a formal methodology wherein the functions of the corresponding state-points in the two circuits are proved to be functionally equivalent. This method is known as formal equivalence checking and it is in the category of verification methods known as formal verification.
Alternatively, simulation refers to the process of simulating only some of the possible excitations on the two circuits to determine that they behave equivalently. However, as all the possible excitations are not tested, this technique can lead to errors in practice. Simulation is considered an informal verification technique.
Conventionally, simulation, although inferior to formal verification, is used to test those circuits that can not be tested using formal techniques. For example, formal techniques cannot be used on circuits with multiple levels of input to output paths. Some example circuits with multiple input and output paths include FPGA, ROM arrays, RAM circuits, and other custom integrated circuit designs.
A typical approach to test multiple levels of input to output paths is to abstract out all the transistors and model them as Boolean functions. However, Boolean functions are incapable of accurately representing all the possible switch situations. Thus, the Boolean model eliminates the ability to natively view and analyze the circuits as they truly function. Verification techniques using these Boolean abstractions are inaccurate and therefore leave potential problems undetected in the finished circuit design.
Therefore, a method to verify a circuit that contain multiple levels of input/output paths is needed. Some embodiments of the invention provide an improved method and system for verification. In some embodiments, a method and system of creating a boolean model of multi-path and multi-strength signals for verification includes: reading a design description of the circuit design, replacing each multi-strength device with logic including encoded output signals, inserting logic into the encoded output signals, applying a Boolean algorithm.